Nuprl Lemma : eqff_to_assert 13,42

b:. (b = ff)  ((b)) 
latex


Upbool 1, bool 1
Definitions, t  T, P  Q, P  Q, P & Q, P  Q, x:AB(x), if b then t else f fi , b, ff, True, tt, b, Unit, , False, A,
Lemmasbnot wf, assert wf, bfalse wf, bool wf, btrue neq bfalse, assert of ff

origin